$\forall$${\it es}$:ES, $A$:Type, $X$:AbsInterface($A$). $X$ is finite $\in$ $\mathbb{P}$